Inference at * 1 1 
Iof proof for Lemma sq stable all:



1. A : Type
2. P : A
3. x:A. (P(x))  P(x)
4. (x:A. P(x))
5. x : A
  P(x) 

latex

 by ((((BasicSquashHD 4) 
CollapseTHEN (TrivializeConcl))) 
CollapseTHEN (SquashCD)) 

latex

C1: 

C1: 4. x:A. P(x)
C1: 5. x : A
C1:   P(x)
C.

Definitions

t  T, True, T